@i Precondition for a(v)
@i P State(ds) (v:T)
== (x:Id. vartype(i;x)  ds(x)?Top)
== & e@i. kind(e) = locl(a)  valtype(e)  T & P((state when e),val(e))
== & & e@i. ee'.kind(e') = locl(a)  (v:T. P(state after e',v))
== & & ((v:T. P(es_init(es)(i),v))  (e:E. loc(e) = i)) 

latex

---

clarification:

pre-p(es;i;ds;a;T;P)
== (x:Id. es-vartype(es; i; x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;i;e.es-kind(es; e) = locl(a)  Knd
== & alle-at(es;i;e. es-valtype(es; e)  T & P(es-state-when(es;e),es-val(es; e)))
== & & alle-at(es;i;e.existse-ge(es;e;e'.es-kind(es; e') = locl(a)  Knd
== & &  (v:T. P(es-state-after(es;e'),v))))
== & & ((v:T. P(es_init(es)(i),v))  (e:es-E(es). es-loc(es; e) = i  Id)) 

latex

Definitions	vartype(i;x), f(x)?z, IdDeq, Top, P & Q, A & B, valtype(e), (state when e), val(e), e@i. P(e), ee'.P(e'), P  Q, Knd, kind(e), locl(a), x:A. B(x), A, state after e, P  Q, f(a), es_init(es), x:A. B(x), E, s = t, Id, loc(e)
FDL editor aliases	pre-p